;; The first four lines of this file were added by Dracula.
;; They tell DrScheme that this is a Dracula Modular ACL2 program.
;; Leave these lines unchanged so that DrScheme can properly load this file.
#reader(planet "reader.rkt" ("cce" "dracula.plt") "modular" "lang")
(interface Iresize
  (sig resize (tr perc))
  
  ; contracts
  (con resize-returns-true-bmp-tree
       (implies (and (bmp-tree? tr) (natp perc)))
       (true-bmp-tree? (resize tr perc)))
  (con resize-200-50-round-trip
       (implies (bmp-tree? tr))
       (equal tr
              (resize (resize tr 200) 50))) 
  )